package ar.edu.utn.frsf.cidisi.upcolbpip.verification;

import java.io.File;
import java.net.InetAddress;
import java.net.URL;

import org.cpntools.accesscpn.engine.DaemonSimulator;
import org.cpntools.accesscpn.engine.Simulator;
import org.cpntools.accesscpn.engine.highlevel.HighLevelSimulator;
import org.cpntools.accesscpn.model.PetriNet;
import org.cpntools.accesscpn.model.importer.DOMParser;

public class StateSpaceTool {
	public static void main(String[] args) throws Exception {
//		String file = args[0];
		String file = "D:\\workspaces\\runtime-upcolbpip-verification\\upcolbpip-test\\model\\andnull.cpn";
		PetriNet petriNet = DOMParser.parse(new URL("file:///" + file));
		HighLevelSimulator s = HighLevelSimulator.getHighLevelSimulator(
		new Simulator(new DaemonSimulator(InetAddress.getLocalHost(), 23456, new File("cpn.ML"))));
		try { 
			CheckerJob checkerJob = new CheckerJob("My model", petriNet, null, s);
			checkerJob.schedule(); checkerJob.join();
			s.evaluate("use \"simple-dfs.sml\"");
			System.out.println(s.evaluate("let val (s, storage) = dfs dead (CPNToolsModel.getInitialStates())" +
					" in (s, HashTable.numItems storage) " +
					"end"));
		} finally {
		s.destroy();
		} 
	} 
}